#!/usr/bin/python
#-*- coding:utf-8 -*-

import re
import random

from struct import unpack

from z3 import *

S= Solver()
k0, k1, k2, k3,k4 = BitVecs("k0 k1 k2 k3 k4", 32)
a=""
S.add(k0 & 0x80808080 == 0)
S.add(k1 & 0x80808080 == 0)
S.add(k2 & 0x80808080 == 0)
#S.add(k3 & 0x80808080 == 0)
S.add(k3 & 0x80808080 == 0)


List = Datatype('List')
List.declare(a, ('car', IntSort()), ('cdr', List))
List.declare('nil')
List = List.create()
S.add(len(str(List.accessor(0, 0)))>2)

print S.check()
m = S.model()
print m

